the_es:ES, e':E, l:IdLnk, m:Msg.
(m  snds(l;before(e')))  (e:E. (e <loc e') & (m  sends(l;e))) 

latex

Definitions	IdLnk, ES, snds(l;before(e)), concat(ll), map(f;as), before(e), x. t(x), P  Q, P  Q, P  Q, Prop, E, x:A. B(x), (e <loc e'), P & Q, (x  l), sends(l;e), S  T, x:A. B(x), (Msg on l), t  T, Msg
Lemmas	es-sends wf, l member wf, es-locl wf, member-es-before, and functionality wrt iff, exists functionality wrt iff, iff functionality wrt iff, map wf, member map, es-Msgl wf, es-before wf, concat wf, member-concat, event system wf, es-E wf, IdLnk wf, es-Msg wf